$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $x$, $y$:$A$, $v$:$B$($x$), $u$:$B$($y$).
\\[0ex]$x$ : $v$ $\parallel$ $y$ : $u$ $\Leftarrow\!\Rightarrow$ (($x$ = $y$) $\Rightarrow$ ($v$ = $u$ $\in$ $B$($x$)))